$E$ $\Lleftarrow\!\Rrightarrow$\{$T$\} ${\it E'}$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$x$, $y$:$T$. ($E$($x$,$y$)) $\Leftarrow\!\Rightarrow$ (${\it E'}$($x$,$y$))